MAYBE 2.898
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could not be shown:
↳ HASKELL
↳ BR
mainModule Main
| ((enumFromThen :: Int -> Int -> [Int]) :: Int -> Int -> [Int]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((enumFromThen :: Int -> Int -> [Int]) :: Int -> Int -> [Int]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ Narrow
mainModule Main
| (enumFromThen :: Int -> Int -> [Int]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_primMinusNat(Succ(vx4000), Succ(vx5000)) → new_primMinusNat(vx4000, vx5000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMinusNat(Succ(vx4000), Succ(vx5000)) → new_primMinusNat(vx4000, vx5000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(vx4000), Succ(vx3000)) → new_primPlusNat(vx4000, vx3000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(vx4000), Succ(vx3000)) → new_primPlusNat(vx4000, vx3000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_primPlusInt(Succ(vx400), Succ(vx300), vx5) → new_primPlusInt(vx400, vx300, vx5)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusInt(Succ(vx400), Succ(vx300), vx5) → new_primPlusInt(vx400, vx300, vx5)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ MNOCProof
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(vx4, vx3, vx5) → new_iterate(vx4, vx3, new_ps(vx4, vx3, vx5))
The TRS R consists of the following rules:
new_primMinusNat3(Succ(vx500)) → Neg(Succ(vx500))
new_primMinusNat0(vx400, Succ(vx500)) → new_primMinusNat1(vx400, vx500)
new_primMinusNat3(Zero) → Pos(Zero)
new_ps(Neg(vx40), Neg(vx30), vx5) → new_primPlusInt0(vx30, vx40, vx5)
new_ps(Neg(Succ(vx400)), Pos(Succ(vx300)), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), Succ(new_primPlusNat3(vx400, vx300)))
new_primPlusNat2(vx400, Zero) → Succ(vx400)
new_primPlusNat3(Succ(vx4000), Zero) → Succ(vx4000)
new_primPlusNat3(Zero, Succ(vx3000)) → Succ(vx3000)
new_primPlusNat0(Zero) → Zero
new_primPlusInt0(Zero, Succ(vx300), Pos(vx50)) → new_primMinusNat2(vx50, vx300)
new_primMinusNat0(vx400, Zero) → Pos(Succ(vx400))
new_primPlusNat3(Zero, Zero) → Zero
new_primMinusNat1(Succ(vx4000), Zero) → Pos(Succ(vx4000))
new_primMinusNat2(Zero, vx300) → Neg(Succ(vx300))
new_ps(Neg(Zero), Pos(Zero), Pos(Zero)) → new_primMinusNat3(Zero)
new_primPlusInt0(Succ(vx400), Succ(vx300), vx5) → new_primPlusInt0(vx400, vx300, vx5)
new_ps(Pos(Zero), Neg(Succ(vx300)), Neg(vx50)) → new_primMinusNat0(vx300, vx50)
new_ps(Pos(Succ(vx400)), Neg(Zero), Neg(vx50)) → new_primMinusNat0(vx400, vx50)
new_ps(Neg(Zero), Pos(Succ(vx300)), Pos(Zero)) → new_primMinusNat2(Zero, vx300)
new_ps(Neg(Succ(vx400)), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, vx400)
new_primPlusNat2(vx400, Succ(vx500)) → Succ(Succ(new_primPlusNat3(vx400, vx500)))
new_ps(Pos(Zero), Neg(Zero), Neg(vx50)) → new_primMinusNat3(vx50)
new_ps(Neg(Succ(vx400)), Pos(Succ(vx300)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat3(vx400, vx300)))
new_primPlusInt0(Zero, Zero, Neg(vx50)) → new_primMinusNat3(vx50)
new_ps(Pos(Succ(vx400)), Neg(Succ(vx300)), Neg(vx50)) → new_primMinusNat0(Succ(new_primPlusNat3(vx400, vx300)), vx50)
new_ps(Neg(Zero), Pos(Zero), Pos(Succ(vx500))) → new_primMinusNat0(vx500, Zero)
new_primMinusNat2(Succ(vx500), vx300) → new_primMinusNat1(vx500, vx300)
new_ps(Pos(vx40), Pos(vx30), vx5) → new_primPlusInt0(vx40, vx30, vx5)
new_ps(Neg(Zero), Pos(Succ(vx300)), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), vx300)
new_ps(Neg(Succ(vx400)), Pos(Zero), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), vx400)
new_primPlusInt0(Zero, Succ(vx300), Neg(vx50)) → Neg(new_primPlusNat2(vx300, vx50))
new_primPlusNat1(Succ(vx400), Succ(vx300), vx50) → new_primPlusNat2(Succ(new_primPlusNat3(vx400, vx300)), vx50)
new_primPlusNat1(Succ(vx400), Zero, vx50) → new_primPlusNat2(vx400, vx50)
new_primPlusNat1(Zero, Succ(vx300), vx50) → new_primPlusNat2(vx300, vx50)
new_primMinusNat1(Zero, Succ(vx5000)) → Neg(Succ(vx5000))
new_ps(Pos(vx40), Neg(vx30), Pos(vx50)) → Pos(new_primPlusNat1(vx40, vx30, vx50))
new_primPlusNat3(Succ(vx4000), Succ(vx3000)) → Succ(Succ(new_primPlusNat3(vx4000, vx3000)))
new_primPlusNat1(Zero, Zero, vx50) → new_primPlusNat0(vx50)
new_ps(Neg(vx40), Pos(vx30), Neg(vx50)) → Neg(new_primPlusNat1(vx40, vx30, vx50))
new_primMinusNat1(Succ(vx4000), Succ(vx5000)) → new_primMinusNat1(vx4000, vx5000)
new_primPlusNat0(Succ(vx500)) → Succ(vx500)
new_primPlusInt0(Succ(vx400), Zero, Neg(vx50)) → new_primMinusNat0(vx400, vx50)
new_primPlusInt0(Succ(vx400), Zero, Pos(vx50)) → Pos(new_primPlusNat2(vx400, vx50))
new_primMinusNat1(Zero, Zero) → Pos(Zero)
new_primPlusInt0(Zero, Zero, Pos(vx50)) → Pos(new_primPlusNat0(vx50))
The set Q consists of the following terms:
new_ps(Pos(x0), Neg(x1), Pos(x2))
new_primPlusInt0(Zero, Zero, Pos(x0))
new_primPlusNat0(Succ(x0))
new_primMinusNat2(Succ(x0), x1)
new_primMinusNat0(x0, Succ(x1))
new_primPlusNat2(x0, Succ(x1))
new_ps(Neg(Zero), Pos(Zero), Pos(Zero))
new_primPlusNat3(Succ(x0), Succ(x1))
new_primPlusInt0(Zero, Succ(x0), Pos(x1))
new_primPlusNat3(Succ(x0), Zero)
new_ps(Pos(Zero), Neg(Succ(x0)), Neg(x1))
new_primMinusNat1(Succ(x0), Succ(x1))
new_ps(Pos(Succ(x0)), Neg(Zero), Neg(x1))
new_ps(Pos(Succ(x0)), Neg(Succ(x1)), Neg(x2))
new_primMinusNat1(Succ(x0), Zero)
new_primPlusInt0(Succ(x0), Zero, Pos(x1))
new_ps(Neg(Zero), Pos(Succ(x0)), Pos(Zero))
new_primPlusNat3(Zero, Zero)
new_primPlusNat1(Zero, Zero, x0)
new_primMinusNat1(Zero, Succ(x0))
new_primMinusNat3(Succ(x0))
new_ps(Neg(Succ(x0)), Pos(Succ(x1)), Pos(Zero))
new_primPlusNat2(x0, Zero)
new_ps(Pos(x0), Pos(x1), x2)
new_ps(Neg(Succ(x0)), Pos(Zero), Pos(Succ(x1)))
new_ps(Neg(Zero), Pos(Succ(x0)), Pos(Succ(x1)))
new_primPlusNat1(Zero, Succ(x0), x1)
new_primPlusNat3(Zero, Succ(x0))
new_ps(Neg(x0), Pos(x1), Neg(x2))
new_primPlusInt0(Zero, Succ(x0), Neg(x1))
new_ps(Neg(Succ(x0)), Pos(Succ(x1)), Pos(Succ(x2)))
new_ps(Neg(x0), Neg(x1), x2)
new_primPlusInt0(Zero, Zero, Neg(x0))
new_primMinusNat0(x0, Zero)
new_primPlusNat1(Succ(x0), Zero, x1)
new_ps(Neg(Zero), Pos(Zero), Pos(Succ(x0)))
new_ps(Neg(Succ(x0)), Pos(Zero), Pos(Zero))
new_primPlusInt0(Succ(x0), Zero, Neg(x1))
new_primMinusNat3(Zero)
new_primPlusNat1(Succ(x0), Succ(x1), x2)
new_primPlusNat0(Zero)
new_primMinusNat2(Zero, x0)
new_primPlusInt0(Succ(x0), Succ(x1), x2)
new_primMinusNat1(Zero, Zero)
new_ps(Pos(Zero), Neg(Zero), Neg(x0))
We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ MNOCProof
↳ QDP
↳ NonTerminationProof
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_iterate(vx4, vx3, vx5) → new_iterate(vx4, vx3, new_ps(vx4, vx3, vx5))
The TRS R consists of the following rules:
new_primMinusNat3(Succ(vx500)) → Neg(Succ(vx500))
new_primMinusNat0(vx400, Succ(vx500)) → new_primMinusNat1(vx400, vx500)
new_primMinusNat3(Zero) → Pos(Zero)
new_ps(Neg(vx40), Neg(vx30), vx5) → new_primPlusInt0(vx30, vx40, vx5)
new_ps(Neg(Succ(vx400)), Pos(Succ(vx300)), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), Succ(new_primPlusNat3(vx400, vx300)))
new_primPlusNat2(vx400, Zero) → Succ(vx400)
new_primPlusNat3(Succ(vx4000), Zero) → Succ(vx4000)
new_primPlusNat3(Zero, Succ(vx3000)) → Succ(vx3000)
new_primPlusNat0(Zero) → Zero
new_primPlusInt0(Zero, Succ(vx300), Pos(vx50)) → new_primMinusNat2(vx50, vx300)
new_primMinusNat0(vx400, Zero) → Pos(Succ(vx400))
new_primPlusNat3(Zero, Zero) → Zero
new_primMinusNat1(Succ(vx4000), Zero) → Pos(Succ(vx4000))
new_primMinusNat2(Zero, vx300) → Neg(Succ(vx300))
new_ps(Neg(Zero), Pos(Zero), Pos(Zero)) → new_primMinusNat3(Zero)
new_primPlusInt0(Succ(vx400), Succ(vx300), vx5) → new_primPlusInt0(vx400, vx300, vx5)
new_ps(Pos(Zero), Neg(Succ(vx300)), Neg(vx50)) → new_primMinusNat0(vx300, vx50)
new_ps(Pos(Succ(vx400)), Neg(Zero), Neg(vx50)) → new_primMinusNat0(vx400, vx50)
new_ps(Neg(Zero), Pos(Succ(vx300)), Pos(Zero)) → new_primMinusNat2(Zero, vx300)
new_ps(Neg(Succ(vx400)), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, vx400)
new_primPlusNat2(vx400, Succ(vx500)) → Succ(Succ(new_primPlusNat3(vx400, vx500)))
new_ps(Pos(Zero), Neg(Zero), Neg(vx50)) → new_primMinusNat3(vx50)
new_ps(Neg(Succ(vx400)), Pos(Succ(vx300)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat3(vx400, vx300)))
new_primPlusInt0(Zero, Zero, Neg(vx50)) → new_primMinusNat3(vx50)
new_ps(Pos(Succ(vx400)), Neg(Succ(vx300)), Neg(vx50)) → new_primMinusNat0(Succ(new_primPlusNat3(vx400, vx300)), vx50)
new_ps(Neg(Zero), Pos(Zero), Pos(Succ(vx500))) → new_primMinusNat0(vx500, Zero)
new_primMinusNat2(Succ(vx500), vx300) → new_primMinusNat1(vx500, vx300)
new_ps(Pos(vx40), Pos(vx30), vx5) → new_primPlusInt0(vx40, vx30, vx5)
new_ps(Neg(Zero), Pos(Succ(vx300)), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), vx300)
new_ps(Neg(Succ(vx400)), Pos(Zero), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), vx400)
new_primPlusInt0(Zero, Succ(vx300), Neg(vx50)) → Neg(new_primPlusNat2(vx300, vx50))
new_primPlusNat1(Succ(vx400), Succ(vx300), vx50) → new_primPlusNat2(Succ(new_primPlusNat3(vx400, vx300)), vx50)
new_primPlusNat1(Succ(vx400), Zero, vx50) → new_primPlusNat2(vx400, vx50)
new_primPlusNat1(Zero, Succ(vx300), vx50) → new_primPlusNat2(vx300, vx50)
new_primMinusNat1(Zero, Succ(vx5000)) → Neg(Succ(vx5000))
new_ps(Pos(vx40), Neg(vx30), Pos(vx50)) → Pos(new_primPlusNat1(vx40, vx30, vx50))
new_primPlusNat3(Succ(vx4000), Succ(vx3000)) → Succ(Succ(new_primPlusNat3(vx4000, vx3000)))
new_primPlusNat1(Zero, Zero, vx50) → new_primPlusNat0(vx50)
new_ps(Neg(vx40), Pos(vx30), Neg(vx50)) → Neg(new_primPlusNat1(vx40, vx30, vx50))
new_primMinusNat1(Succ(vx4000), Succ(vx5000)) → new_primMinusNat1(vx4000, vx5000)
new_primPlusNat0(Succ(vx500)) → Succ(vx500)
new_primPlusInt0(Succ(vx400), Zero, Neg(vx50)) → new_primMinusNat0(vx400, vx50)
new_primPlusInt0(Succ(vx400), Zero, Pos(vx50)) → Pos(new_primPlusNat2(vx400, vx50))
new_primMinusNat1(Zero, Zero) → Pos(Zero)
new_primPlusInt0(Zero, Zero, Pos(vx50)) → Pos(new_primPlusNat0(vx50))
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
new_iterate(vx4, vx3, vx5) → new_iterate(vx4, vx3, new_ps(vx4, vx3, vx5))
The TRS R consists of the following rules:
new_primMinusNat3(Succ(vx500)) → Neg(Succ(vx500))
new_primMinusNat0(vx400, Succ(vx500)) → new_primMinusNat1(vx400, vx500)
new_primMinusNat3(Zero) → Pos(Zero)
new_ps(Neg(vx40), Neg(vx30), vx5) → new_primPlusInt0(vx30, vx40, vx5)
new_ps(Neg(Succ(vx400)), Pos(Succ(vx300)), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), Succ(new_primPlusNat3(vx400, vx300)))
new_primPlusNat2(vx400, Zero) → Succ(vx400)
new_primPlusNat3(Succ(vx4000), Zero) → Succ(vx4000)
new_primPlusNat3(Zero, Succ(vx3000)) → Succ(vx3000)
new_primPlusNat0(Zero) → Zero
new_primPlusInt0(Zero, Succ(vx300), Pos(vx50)) → new_primMinusNat2(vx50, vx300)
new_primMinusNat0(vx400, Zero) → Pos(Succ(vx400))
new_primPlusNat3(Zero, Zero) → Zero
new_primMinusNat1(Succ(vx4000), Zero) → Pos(Succ(vx4000))
new_primMinusNat2(Zero, vx300) → Neg(Succ(vx300))
new_ps(Neg(Zero), Pos(Zero), Pos(Zero)) → new_primMinusNat3(Zero)
new_primPlusInt0(Succ(vx400), Succ(vx300), vx5) → new_primPlusInt0(vx400, vx300, vx5)
new_ps(Pos(Zero), Neg(Succ(vx300)), Neg(vx50)) → new_primMinusNat0(vx300, vx50)
new_ps(Pos(Succ(vx400)), Neg(Zero), Neg(vx50)) → new_primMinusNat0(vx400, vx50)
new_ps(Neg(Zero), Pos(Succ(vx300)), Pos(Zero)) → new_primMinusNat2(Zero, vx300)
new_ps(Neg(Succ(vx400)), Pos(Zero), Pos(Zero)) → new_primMinusNat2(Zero, vx400)
new_primPlusNat2(vx400, Succ(vx500)) → Succ(Succ(new_primPlusNat3(vx400, vx500)))
new_ps(Pos(Zero), Neg(Zero), Neg(vx50)) → new_primMinusNat3(vx50)
new_ps(Neg(Succ(vx400)), Pos(Succ(vx300)), Pos(Zero)) → new_primMinusNat2(Zero, Succ(new_primPlusNat3(vx400, vx300)))
new_primPlusInt0(Zero, Zero, Neg(vx50)) → new_primMinusNat3(vx50)
new_ps(Pos(Succ(vx400)), Neg(Succ(vx300)), Neg(vx50)) → new_primMinusNat0(Succ(new_primPlusNat3(vx400, vx300)), vx50)
new_ps(Neg(Zero), Pos(Zero), Pos(Succ(vx500))) → new_primMinusNat0(vx500, Zero)
new_primMinusNat2(Succ(vx500), vx300) → new_primMinusNat1(vx500, vx300)
new_ps(Pos(vx40), Pos(vx30), vx5) → new_primPlusInt0(vx40, vx30, vx5)
new_ps(Neg(Zero), Pos(Succ(vx300)), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), vx300)
new_ps(Neg(Succ(vx400)), Pos(Zero), Pos(Succ(vx500))) → new_primMinusNat2(Succ(vx500), vx400)
new_primPlusInt0(Zero, Succ(vx300), Neg(vx50)) → Neg(new_primPlusNat2(vx300, vx50))
new_primPlusNat1(Succ(vx400), Succ(vx300), vx50) → new_primPlusNat2(Succ(new_primPlusNat3(vx400, vx300)), vx50)
new_primPlusNat1(Succ(vx400), Zero, vx50) → new_primPlusNat2(vx400, vx50)
new_primPlusNat1(Zero, Succ(vx300), vx50) → new_primPlusNat2(vx300, vx50)
new_primMinusNat1(Zero, Succ(vx5000)) → Neg(Succ(vx5000))
new_ps(Pos(vx40), Neg(vx30), Pos(vx50)) → Pos(new_primPlusNat1(vx40, vx30, vx50))
new_primPlusNat3(Succ(vx4000), Succ(vx3000)) → Succ(Succ(new_primPlusNat3(vx4000, vx3000)))
new_primPlusNat1(Zero, Zero, vx50) → new_primPlusNat0(vx50)
new_ps(Neg(vx40), Pos(vx30), Neg(vx50)) → Neg(new_primPlusNat1(vx40, vx30, vx50))
new_primMinusNat1(Succ(vx4000), Succ(vx5000)) → new_primMinusNat1(vx4000, vx5000)
new_primPlusNat0(Succ(vx500)) → Succ(vx500)
new_primPlusInt0(Succ(vx400), Zero, Neg(vx50)) → new_primMinusNat0(vx400, vx50)
new_primPlusInt0(Succ(vx400), Zero, Pos(vx50)) → Pos(new_primPlusNat2(vx400, vx50))
new_primMinusNat1(Zero, Zero) → Pos(Zero)
new_primPlusInt0(Zero, Zero, Pos(vx50)) → Pos(new_primPlusNat0(vx50))
s = new_iterate(vx4, vx3, vx5) evaluates to t =new_iterate(vx4, vx3, new_ps(vx4, vx3, vx5))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [vx5 / new_ps(vx4, vx3, vx5)]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from new_iterate(vx4, vx3, vx5) to new_iterate(vx4, vx3, new_ps(vx4, vx3, vx5)).
Haskell To QDPs